↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → U21(X, X1, X2, Right, tree_member_in(X, Right))
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → U11(X, X1, Left, X2, tree_member_in(X, Left))
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → U21(X, X1, X2, Right, tree_member_in(X, Right))
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → U11(X, X1, Left, X2, tree_member_in(X, Left))
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
TREE_MEMBER_IN(X) → TREE_MEMBER_IN(X)
TREE_MEMBER_IN(X) → TREE_MEMBER_IN(X)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → U21(X, X1, X2, Right, tree_member_in(X, Right))
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → U11(X, X1, Left, X2, tree_member_in(X, Left))
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → U21(X, X1, X2, Right, tree_member_in(X, Right))
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → U11(X, X1, Left, X2, tree_member_in(X, Left))
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
tree_member_in(X, tree(X1, X2, Right)) → U2(X, X1, X2, Right, tree_member_in(X, Right))
tree_member_in(X, tree(X1, Left, X2)) → U1(X, X1, Left, X2, tree_member_in(X, Left))
tree_member_in(X, tree(X, X1, X2)) → tree_member_out(X, tree(X, X1, X2))
U1(X, X1, Left, X2, tree_member_out(X, Left)) → tree_member_out(X, tree(X1, Left, X2))
U2(X, X1, X2, Right, tree_member_out(X, Right)) → tree_member_out(X, tree(X1, X2, Right))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
TREE_MEMBER_IN(X, tree(X1, Left, X2)) → TREE_MEMBER_IN(X, Left)
TREE_MEMBER_IN(X, tree(X1, X2, Right)) → TREE_MEMBER_IN(X, Right)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
TREE_MEMBER_IN(X) → TREE_MEMBER_IN(X)
TREE_MEMBER_IN(X) → TREE_MEMBER_IN(X)